This session is about, or this day is about cyberphysical systems or embedded systems

and I will talk about a particular aspect, namely how to verify that a system is reacting

in time.

So you all know lots of embedded real-time systems in your environment, in your car you

have a lot, in planes there are a lot of real-time systems and they have deadlines within which

they have to react.

And these deadlines, for instance in the automotive area go down to the microsecond level.

So there's not much time and sometimes considerable computation.

So the question is how to prove that the system reacts within its deadline.

So a particular emphasis in this talk is about multi-core platforms.

So the embedded systems industry goes over to multi-core platforms and they have certain

advantages.

But the problem is currently, I will come to that later, the problem is that there is

currently no sound method to verify the real-time behavior of multi-core platforms.

Okay this is the structure of the talk.

So I will first define the problem and then our solution in the single core case.

Then I will discuss which approaches currently people are taking, some approaches to deal

with the multi-core problem and in the end come up with some speculative ideas.

What could be a solution?

Okay the problem is in a simpler setting you have the following, you have a terminating

software which is supposed to produce a reaction upon a stimulus.

In the first setting a single core hardware platform on which you execute the software,

there's a given deadline for the reaction and you have to derive a guarantee for the

timeliness.

The system should under all circumstances react within the deadline.

Very simple problem.

There are lots of variants.

So this assumes uninterrupted execution but you may interrupt, you may preempt, you may

have tasks that share resources.

It will come to more complicated settings.

This is the simplest one and I will tell you what we did about this.

Okay so if you think about what it means to determine a safe bound on all execution times,

you could think of this as a graph problem, namely searching for longest paths in a appropriate

graph.

And I will show you that depending on the architecture there are different types of

graphs you have to search.

So I will show you that there are different types and that depending on the architecture

the size of these graphs is quite different and maybe quite huge.

So I will tell you how this huge state space originates and I will tell you how to cope

with it.

And decidability here, we don't solve the Turing, the holding problem.

Decidability is guaranteed.

Everything is finite but large and complexity is a problem.

So in the historic case, if you look at old books on embedded systems they say don't use

a processor with a cache pipeline speculation.

So use a simple microcontroller.

In those times you only had to look at the control flow path of the program and you looked

for the longest path in the control flow graph assuming that iteration and recursion are

bounded.

Okay, again we don't want to solve the holding problem.